Nuprl Lemma : find_wf
4,23
postcript
pdf
T
:Type,
P
:(
T
),
as
:
T
List,
d
:
T
. (first
a
as
s.t.
P
(
a
) else
d
)
T
latex
Definitions
t
T
,
,
x
(
s
)
,
x
:
A
.
B
(
x
)
,
filter(
P
;
l
)
,
first
x
as
s.t.
P
(
x
) else
d
Lemmas
filter
wf
,
bool
wf
origin
T:Type, P:(T
), as:T List, d:T. (first a 
as s.t. P(a) else d) T T:Type, P:(T), as:T List, d:T. (first a as s.t. P(a) else d) T Tx:A. B(x) as s.t. P(x) else d